#! /bin/sh

echo "Tests on kripke_examples/very_simple :"

echo "AX(w) :"
./model_checker ./test/kripke_examples/very_simple "AX(w)" > /dev/null
if [ $? -eq 1 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "EX(w) :"
./model_checker ./test/kripke_examples/very_simple "EX(w)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "AF(w) :"
./model_checker test/kripke_examples/very_simple "AF(w)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "EF(w) :"
./model_checker test/kripke_examples/very_simple "EF(w)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo ""
echo "Tests on test/kripke_examples/cl3serv1.kripke :"

echo "AG(IMPLIES(w1,AF(s1))) :"
./model_checker test/kripke_examples/cl3serv1.kripke "AG(IMPLIES(w1,AF(s1)))" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi


echo ""
echo "Tests on test/kripke_examples/cl3serv3.kripke :"

echo "AG(IMPLIES(w1,AF(s1))) :"
./model_checker test/kripke_examples/cl3serv3.kripke "AG(IMPLIES(w1,AF(s1)))" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi


echo ""
echo "Tests on test/kripke_examples/eeaean1.kripke :"

echo "EF(threeLeads) :"
./model_checker test/kripke_examples/eeaean1.kripke "EF(threeLeads)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "EU(noLeader, zeroLeads) :"
./model_checker test/kripke_examples/eeaean1.kripke "EU(noLeader, zeroLeads)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "AG(IMPLIES(noLeader,AF(zeroLeads))) :"
./model_checker test/kripke_examples/eeaean1.kripke "AG(IMPLIES(noLeader,AF(zeroLeads)))" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi



echo ""
echo "Tests on test/kripke_examples/eeaean2.kripke :"

echo "EF(threeLeads) :"
./model_checker test/kripke_examples/eeaean2.kripke "EF(threeLeads)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "EU(noLeader, zeroLeads) :"
./model_checker test/kripke_examples/eeaean2.kripke "EU(noLeader, zeroLeads)" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi

echo "AG(IMPLIES(noLeader,AF(zeroLeads))) :"
./model_checker test/kripke_examples/eeaean2.kripke "AG(IMPLIES(noLeader,AF(zeroLeads)))" > /dev/null
if [ $? -eq 0 ]
then
    echo "OK"
else
    echo "KO"
fi
